$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$), $x$:Id.
\\[0ex]($\uparrow$es{-}first(${\it es}$; $e$))
\\[0ex]$\Rightarrow$ sqequal(es{-}when(${\it es}$; $x$; $e$); (es\_init(${\it es}$)(loc($e$),$x$,0 + es{-}time(${\it es}$; $e$))))